M:msga{i:l}. ma-feasible{i:l}(M)  {i'} 

latex

Definitions	x,y. t(x;y), x. t(x), t.2, t.1, P & Q, Feasible(M), , t  T, x:A. B(x), x(s1,s2), x(s), Valtype(da;k), MsgA
Lemmas	msga wf, ma-frame-compat wf, ma-prob-da wf, decidable wf, Kind-deq wf, Knd wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, id-deq wf, Id wf, fpf-all wf